
; Copyright (c) 2015 Microsoft Corporation
(declare-fun p1 () Bool)
(declare-fun p2 () Bool)
(declare-fun p3 () Bool)
(declare-fun p4 () Bool)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)

(set-option :pp.flat-assoc false)
(echo "Testing basic...")
(dbg-bool-rewriter true)
(dbg-bool-rewriter (not true))
(dbg-bool-rewriter (not false))
(echo "Testing eq...")
(dbg-bool-rewriter (= a a))
(dbg-bool-rewriter (= a b))
(dbg-bool-rewriter (not (= a a)))
(dbg-bool-rewriter (= p1 true))
(dbg-bool-rewriter (= p1 false))
(dbg-bool-rewriter (= p1 (not p1)))
(dbg-bool-rewriter (= (not p2) (not p1)))
(dbg-bool-rewriter (= (not (not p2)) (not (not p1))))
(dbg-bool-rewriter (= (not (not p1)) (not (not p2))))
(dbg-bool-rewriter (not (= (not (not p1)) (not (not p2)))))
(dbg-bool-rewriter (= true p2))
(dbg-bool-rewriter (= false p2))
(dbg-bool-rewriter (= 0 1))
(echo "Testing distinct...")
(dbg-bool-rewriter (distinct a))
(dbg-bool-rewriter (distinct a b))
(dbg-bool-rewriter (distinct a a))
(dbg-bool-rewriter (distinct a b c))
(dbg-bool-rewriter (distinct a b a c))
(dbg-bool-rewriter (distinct a b c d b))
(dbg-bool-rewriter (distinct a b c b d))
(dbg-bool-rewriter (distinct a b c d))
(echo "Testing syntax sugar...")
(dbg-bool-rewriter (xor p1 p2))
(dbg-bool-rewriter (xor p1 p2 p3))
(dbg-bool-rewriter (implies p1 p2))

